Nuprl Lemma : l_disjoint_append2
11,40
postcript
pdf
T
:Type,
a
,
b
,
c
:(
T
List). l_disjoint(
T
;
b
@
c
;
a
)
(l_disjoint(
T
;
b
;
a
) & l_disjoint(
T
;
c
;
a
))
latex
Definitions
(
x
l
)
,
P
&
Q
,
P
Q
,
False
,
A
,
P
Q
,
x
:
A
.
B
(
x
)
,
t
T
,
,
P
Q
,
P
Q
,
as
@
bs
,
x
.
t
(
x
)
,
l_disjoint(
T
;
l1
;
l2
)
,
{
T
}
Lemmas
iff
functionality
wrt
iff
,
all
functionality
wrt
iff
,
not
functionality
wrt
iff
,
and
functionality
wrt
iff
,
member
append
,
iff
wf
,
append
wf
,
not
wf
,
l
member
wf
origin
T:Type, a, b, c:(T List). l_disjoint(T;b @ c;a) 
(l_disjoint(T;b;a) & l_disjoint(T;c;a)) T:Type, a, b, c:(T List). l_disjoint(T;b @ c;a) (l_disjoint(T;b;a) & l_disjoint(T;c;a)) 
l) Q
A
Qx:A. B(x) T
Q Q
x. t(x)